#!/bin/bash

if [ -z "$1" ]; then
    echo "Usage: $0 <STRATEGY> [path/to/test.coma]"
    echo "STRATEGY is the strategy to use, for example Auto_level_2"
    echo "If no path to a specific coma file is passed, tries to regenerate all tests in the testsuite"
    echo "If a path to a coma file is passed, tries to regenerate this test only"
    exit 1
fi

eval $(cargo run --bin dev-env)

if [ -z "$2" ]; then
    # upgrade all
    failed=()

    shopt -s globstar
    for file in creusot/tests/**/*.coma; do
        # only try to upgrade if it looks like there is a session directory
        SESSION_DIR="$(dirname $file)/$(basename $file .coma)"
        if [ -d "$SESSION_DIR" ]; then
            echo "==> Regenerating $file"
            why3_tools regenerate -L. "$file" "$1"
            if [ $? != 0 ]; then
                failed+=("$file")
            fi
        fi
    done
    if [ ${#failed[@]} != 0 ]; then
        echo ""
        echo "Failed to regenerate the following tests:"
        printf "%s\n" "${failed[@]}"
    fi
else
    # upgrade a specific test
    echo "==> Regenerating $2"
    why3_tools regenerate -L. "$2" "$1"
fi
